Nuprl Definition : Q-R-glues 11,40

g glues Ia:Qa f Ib:Rb
== {Ia} = g== {Ib} & g is Qa-Rb-pre-preserving on {Ib}
== & Inj({e:E| (e  Ib)} ;E;g)
== & (e:E(Ib). f(g(e)) = Ib(e)) 
latex



clarification:

Q-R-glues(es;Ib_valtype;g;f;Ia;Qa;Ib;Rb)
== weak-antecedent-surjection(es;{Ib};{Ia};g) & Q-R-pre-preserving(es;g;{Ib};Qa;Rb)
== & Inj({e:es-E(es)| (e  Ib)} ;es-E(es);g)
== & (e:es-E-interface(es;Ib). f(g(e)) = Ib(e)  Ib_valtype) 
latex


DefinitionsQ = f== P, f is Q-R-pre-preserving on P, {I}, P & Q, Inj(A;B;f), {x:A| B(x)} , b, e  X, E, x:A. B(x), E(X), s = t, f(a), X(e)
FDL editor aliasesQ-R-glues

origin